#ifndef _PDTCHECKSPECMAINWINDOW_H_
#define _PDTCHECKSPECMAINWINDOW_H_

#include <QMainWindow>

#include <QAbstractItemModel>
#include <QModelIndex>
#include <QVariant>

#include <PDTNode.h>
#include <PDTCheckSpec.h>
#include <map>
using namespace std;

class QAction;
class QListWidget;
class QMenu;
class QTextEdit;
class QTreeView;

class PDTCodeGraph;
class PDTCheckSpec;

class PDTPreCondition;
class PDTPostCondition;
class PDTBehaviors;
class PDTCheckSpecMainWindow;

class PDTSpecTriple  : public PDTNode { public:
    PDTPreCondition * pre;
    PDTPostCondition * post;
    PDTBehaviors * behaviors;

    PDTSpecTriple() :
        pre(NULL), post(NULL), behaviors(NULL)
    {}

    bool hasChildren() const {
        return pre != NULL || post != NULL || behaviors != NULL;
    }
    virtual bool operator == (const PDTSpecTriple & rhs) const {
        return (pre == rhs.pre) && (post == rhs.post) && (behaviors== rhs.behaviors);
    }

    PDTNode * getNodeFromRow(unsigned int row) const;
    unsigned int numChildren() const;
    const string & name() const;

    virtual bool isSpecTriple() const {return true;}
	virtual NodeTypeEnum getType() {return PDTSpecTriple_Em;}

    virtual Traversal::RetType traverseEx(Traversal& t) {
        return Traversal::Skip;
    }
    virtual stringstream& toString(std::stringstream& ss) const {
        return ss;
    }

};

class ResultItemModel : public QAbstractItemModel {
    Q_OBJECT
    public:
        PDTCheckSpecMainWindow & cSpecMW;
        ResultItemModel(PDTCheckSpecMainWindow & csmw) :
            cSpecMW(csmw)
    {       
    }
        /*
           good/bad   number
             advice   text! 
             p(i)     true/false
             q(i,o)   true/false
             q(i,o')  true/false   --- if with code
             o == o'  true/false   --- if with code
             values                
                var   value-of-var

           */
        typedef enum {
            BehaviorItem, AdviceItem, 
            PofIItem, QofIOItem, QofIOprimeItem, OeqOprimeItem, 
            ValuesItem, VarItem,
            LastItemType
        } ItemType;

        struct IID {
            unsigned int type : 3;
            unsigned int withCode : 1;
            unsigned int resultId : 10;
            unsigned int varId : 10;
            unsigned int unused : 8;
            IID(unsigned int t, unsigned int r, 
                    bool c = false, unsigned int v = 0) : 
                type(t), withCode(c?1:0), resultId(r), varId(v),
                    unused(0)
                {
            }
            IID(unsigned int iid) {
                (*this) = *(IID*)(&iid);
            }
            unsigned int uint() {return *(unsigned int*)(this);}
        };
    QVariant headerData(int section, Qt::Orientation orientation,
            int role = Qt::DisplayRole) const;
    int rowCount(const QModelIndex &parent = QModelIndex()) const;
    int columnCount(const QModelIndex &parent = QModelIndex()) const;
    QModelIndex parent(const QModelIndex &index) const;
    QVariant data(const QModelIndex &index, int role) const;
    Qt::ItemFlags flags(const QModelIndex &index) const;

    QModelIndex index(int row, int column,
            const QModelIndex &parent = QModelIndex()) const;
};


class SpecItemModel : public QAbstractItemModel
{
    Q_OBJECT
    public:
        PDTCheckSpecMainWindow & cSpecMW;
        SpecItemModel (PDTCheckSpecMainWindow & csmw) :
            cSpecMW(csmw) 
    {
    }

    QVariant headerData(int section, Qt::Orientation orientation,
            int role = Qt::DisplayRole) const;
    int rowCount(const QModelIndex &parent = QModelIndex()) const;
    int columnCount(const QModelIndex &parent = QModelIndex()) const;
    QModelIndex parent(const QModelIndex &index) const;
    QVariant data(const QModelIndex &index, int role) const;
    Qt::ItemFlags flags(const QModelIndex &index) const;

    QModelIndex index(int row, int column,
            const QModelIndex &parent = QModelIndex()) const;

    string getString(PDTNode * node) const ;
/*
   level = 0: specTripleItem
   level = 1, row = 0: pre item
   level = 1, row = 1: post item
   level = 1, row = 2: behaviors item
   level = 2, row = i: i-th behavior item
   level = 3, row = 0: input item
   level = 3, row = 1: output item
   */
    PDTSpecTriple* getSpecTriple(unsigned int row) const ;
    QModelIndex makeParentSpecIdxModel (const string & name) const;
};

typedef map<string, PDTSpecTriple> SpecTripleMap;

class PDTCheckSpecMainWindow : public QMainWindow
{
    Q_OBJECT

    public:
        PDTCheckSpecMainWindow();
        virtual ~PDTCheckSpecMainWindow();
        void setText(const QString & );

        private slots:
            void newFile();
        void openFile();
        void save();
        void undo();

        void parse();
        void check();
        void checkCode();

        void about();
        void resultChanged (const QString &customer);
        void behaviorChanged(const QString &paragraph);

    private:
        void createActions();
        void createMenus();
        void createToolBars();
        void createStatusBar();
        void createDockWindows();

        void openFileEx();
        void clean() ;
        bool getInfoFromNode(PDTNode * node, PDTSpecTriple *& spec, PDTFunctionDec * & func, PDTBehavior * & beh);

        QString fileName;
        PDTCodeGraph * cg;
        PDTCheckSpec * sCheck;

        QTextEdit *codeEdit;
        QTreeView *specTree;
        QTreeView *resultTree;

        QMenu *fileMenu;
        QMenu *editMenu;
        QMenu *viewMenu;
        QMenu *checkMenu;
        QMenu *helpMenu;

        QToolBar *fileToolBar;
        QToolBar *editToolBar;
        QToolBar *checkToolBar;

        QAction *newFileAct;
        QAction *openFileAct;
        QAction *saveAct;
        QAction *undoAct;
        QAction *aboutAct;
        QAction *quitAct;

        QAction *parseAct;
        QAction *checkAct;
        QAction *checkCodeAct;

        SpecItemModel * sIModel;
        ResultItemModel * rIModel;
    public:
        SpecTripleMap stMap;
        vector <PDTCheckSpec::Result> results;
        vector < vector <PDTVar *> > resultVars;
        vector < vector <PDTConst *> > resultValues;
};

#endif
